Nuprl Lemma : zip_length
4,23
postcript
pdf
T1
,
T2
:Type,
as
:
T1
List,
bs
:
T2
List. ||zip(
as
;
bs
)||
||
as
|| & ||zip(
as
;
bs
)||
||
bs
||
latex
Definitions
i
j
,
||
as
||
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
t
T
,
t
...$L
,
zip(
as
;
bs
)
,
P
Q
,
False
,
A
,
A
B
Lemmas
zip
wf
,
length
nil
,
non
neg
length
,
length
wf1
origin
T1, T2:Type, as:T1 List, bs:T2 List. ||zip(as;bs)||
||as|| & ||zip(as;bs)||||bs|| T1, T2:Type, as:T1 List, bs:T2 List. ||zip(as;bs)||||as|| & ||zip(as;bs)||||bs|| 
jx:A. B(x)
T
Q
AB